feat: runtime primitives for mpz objects #6395
Conversation
tydeu
force-pushed
the
lean-mpz-primitives
branch
3 times, most recently
from
69ed417 to
4a08e12
Compare
github-actions
bot
added
the
toolchain-available
|
Mathlib CI status (docs):
|
leanprover-community-bot
added
the
builds-mathlib
|
Recall that we should be able to build Lean with and without GMP: https://github.com/leanprover/lean4/blob/master/src/CMakeLists.txt#L77 |
|
@leodemoura Yep! The good news is that these primitives are abstracted above the MPZ implementation. (They work with either GMP or our homegrown multiple precision integer implementation.) |
tydeu
force-pushed
the
lean-mpz-primitives
branch
from
e453b34 to
ea15ca7
Compare
tydeu
force-pushed
the
lean-mpz-primitives
branch
from
ea15ca7 to
dc5e674
Compare
| static inline int64_t lean_scalar_to_int64(b_lean_obj_arg a) { | ||
| assert(lean_is_scalar(a)); | ||
| if (sizeof(void*) == 8) | ||
| return (int)((unsigned)lean_unbox(a)); /* NOLINT */ |
There was a problem hiding this comment.
Isn't this truncating to 32 bits?
There was a problem hiding this comment.
@eric-wieser Scalar integers in the Lean runtime are <= 32 bits. These definitions were just moved up.
|
|
||
| extern "C" LEAN_EXPORT obj_res lean_mpz_of_int32(uint32_t n) { | ||
| static_assert(sizeof(uint32_t) <= sizeof(int), "int should be at least the size of a uint32"); | ||
| return alloc_mpz(mpz(static_cast<int>(static_cast<int32_t>(n)))); |
There was a problem hiding this comment.
Why the pair of casts vs letting a constructor overload handle it?
There was a problem hiding this comment.
@eric-wieser There is not int32_t/int32 constructor for mpz. I also wanted to avoid changes to the mpz implentation, focusing instead on just the public API.
There was a problem hiding this comment.
However, perhaps adding more constructor overloads to mpz would be clearer?
This PR adds a basic C API interface for Lean MPZ objects. It includes constructors, conversions, and comparison operators.
These primitives are necessary to correctly and efficiently model runtime MPZ objects in Lean.
Where applicable, existing APIs were adjusted to use the new interface.